A Binary Decision Diagram (BDD) is a data structure that may be used to represent a Boolean function. A Reduced Ordered Binary Decision Diagram (ROBDD) is an optimized BDD that has no redundant nodes and isomorphic sub-graphs and that the variables appear in the same order along each path from root to a terminal node. The size of a BDD is determined by both the Boolean function it represents and the order of the variables of the function. Consequently, variable ordering exposes a critical optimization problem as the size of a BDD often varies greatly as its variable order changes.